|
|
Application of Software Components in Operating System Design
Děcký, Martin ; Tůma, Petr (vedoucí práce) ; Döbel, Björn (oponent) ; Sojka, Michal (oponent)
Tato doktorská práce popisuje primární cíl mikrojádrového multiserverového operačního systému HelenOS. Primárním cílem projektu HelenOS je vytvoření komplexní výzkumné a vývojové platformy pro doménu obecných operačních systémů, která by podporovala nejmodernější přístupy a metody (například verifikaci správnosti) a současně kladla důraz na praktickou relevanci. Text práce popisuje jaké konkrétní prostředky návrhu (založené na softwarových komponentách), implementace, vývojového procesu a verifikace, které jsou použity pro dosažení primárního cíle. Text práce dále hodnotí současný stav projektu HelenOS. Powered by TCPDF (www.tcpdf.org)
|
|
|
Heuristická redukce paralelismu v prostředí komponenty
Pařízek, P. ; Plášil, František
Při model checkingu kódu softwarových komponent, které se vyznačují vysokou úrovní paralelismu, se často vyskytne problem exploze stavového prostoru, bez ohledu na to, že jedna komponenta má obvykle menší stavový prostor než celý systém. Zde prezentujeme techniku, která adresuje problém exploze stavového prostoru pro ověřování kódu primitivních komponent s Java PathFinder v případě, že ověřovaná vlastnost je absence synchronizačních chyb. Klíčová myšlenka je redukce paralelismu v prostředí komponenty tak, že pouze ty části kódu komponenty, které pravděpodobně mohou vyvolat synchronizační chybu, jsou vykonány paralelně; takové části jsou identifikovány pomocí heuristické statické analýzy kódu (hledáním podezřelých vzorů v kódu komponenty). Výhody této techniky, t.j. podpora objevení synchronizačních chyb v omezeném čase a prostoru a reportování čitelnějších protipříkladů, jsou ilustrovány na výsledcích několika experimentů.
|
|
|
Model checking softwarových komponent: úprava Java PathFinder pro spolupráci s Behavior Protocol Checker
Pařízek, P. ; Plášil, František ; Kofroň, Jan
Přestože existuje několik model checkerů pro software, které ověřují kód proti specifikaci zapsané např. v temporální logice a tzv. assertions, nebo ověřují nízkoúrovňové vlastnosti (jako neošetřené výjimky), žádný z nich nepodporuje ověřování softwarových komponent proti vyšší specifikaci chování. Tato zpráva popisuje náš přístup k model checkingu softwarových komponent implementovaných v jazyce Java proti specifikaci jejich chování definované pomocí protokolů chování, který využívá model checker Java PathFinder a protocol checker. Vlastnosti ověřované nástrojem Java PathFinder (korektnost sekvencí volání metod) se validují pomocí spolupráci s nástrojem protocol checker. Ukazujeme, že pouze návrhový vzor publisher/listener, označovaný za klíčový pro podporu rozšiřitelnosti v nástroji Java PathFinder, nebyl dostatečný pro tento typ ověřování (přestože byl pro nás velmi užitečný).
|
|
|
Rozšíření Behavior Protocols o data a multisynchronizaci
Kofroň, Jan
Použití Behavior Protocols pro specifikaci chování komponent v hierarchických komponentových modelech (SOFA, Fractal) se ukázalo být vhodným přístupem, pokud nás zajímá absence komunikačních chyb mezi komponentami v dané aplikaci. Během specifikace Fractalové komponentové aplikace zaměřené na kontrolu přístupu k internetu na letištích umožňující několik způsobů úhrady se projevilo několik nedostatků Behavior Protocols jako specifikační platformy. Dvě nejdůležitější zahrnují (i) nedostatečná vyjadřovací síla Behavior Protocols při specifikaci některých běžných vzorů chování a (ii) nedostatečný výkon aplikace Behavior Protocol Checker – nástroje použitého pro hledání kompozičních chyb mezi komunikujícími komponentami. Tento článek se soustředí na řešení prvního problému pomocí rozšíření formalismu Behavior Protocols.
|
|
|
Ověřování softwarových komponent: O překladu Behavior Protocols do Promely
Kofroň, Jan
Používání softwarových komponent patří k moderním přístupům k vytváření rozšiřitelných a spolehlivých aplikací. K zajištění vysoké spolehlivost by komponentová aplikace měla být verifikována, např. podstoupit model checking. Implementace aplikace je většinou příliš složitá, než aby mohla být verifikována na formální úrovni. Proto se používá model, který je abstrakcí této implementace. Behavior Protocols jsou platformou pro modelování chování softwarových komponent. V tomto článku navrhujeme metodu pro překlad specifikace Behavior Protocols do Promely, která je následně použita jako vstup pro model checker Spin. Pokud máme model v jazyku Promela popisující chování komponent, můžeme efektivně ověřovat kompatibilitu i LTL vlastnosti kooperujících komponent.
|
|
| |
|
| |
|
| |
|
| |
|
| |
host ::
RSS.